Inference at * 1 
Iof proof for Lemma eqtt to assert:



1. b : 
2. b = tt
  b 

latex

 by BoolInd 1 

latex

 1: 

 1: 1. tt = tt
 1:   tt
 2: 

 2: 1. ff = tt
 2:   ff
 .

Definitions

t  T, Unit, , ff, , tt